NoEtaEqualityInductiveRecord.agda:17,10-14
w != c (p w) of type R
when checking that the expression refl has type w ≡ c (p w)
